MA:MsgA, s:MA.state, k:Knd, l:IdLnk, vaal:MA.V(k), i:Id.
source(l) = i
 MA.send(k;
 l;s;vaal;map(x.2of(x);filter(ms.eqof(IdLnkDeq)(mlnk(ms),l);MA.sends(k,s,vaal)));i) 

latex

Definitions

M.sends(k,s,v), x:A. B(x), P  Q, Id, IdLnk, Knd, t  T, MsgA, M.state, M.V(k), M.send(k;l;s;v;ms;i), Valtype(da;k), M.da(a), z != f(x)  P(a;z), a:A fp B(a), State(ds), x(s), b, x  dom(f), x(s1,s2), filter(P;l), mlnk(m), tagged-messages(l;s;v;L), fpf-vals(eq;P;f), eqof(d), concat(ll), map(f;as), 1of(t), 2of(t), f(x), product-deq(A;B;a;b), KindDeq, IdLnkDeq, Top, x. t(x), , tagged-list-messages(s;v;L), A List, P  Q, P & Q, P  Q, S  T, f o g, Unit, Prop, b, A, False, p  q, as @ bs, T, True, S  T, ||as||, if b t else f fi, null(as), hd(l), ij, AB, f(x)?z, rcv(l,tg), source(l), a = b

Lemmas

fpf-cap-void-subtype, eq id wf, assert-eq-id, not functionality wrt iff, lsrc wf, ma-valtype wf, rcv wf, fpf-cap wf, non neg length, hd wf, null wf, ifthenelse wf, length wf1, true wf, squash wf, map-concat, fpf-ap wf, append-nil, assert of band, band wf, fpf-vals-singleton, filter-fpf-vals, subtype rel product, subtype rel list, tagged-list-messages wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, top wf, map-map, concat wf, subtype rel self, deq property, pi1 wf, eqof wf, fpf-vals wf, assert wf, pi2 wf, Id wf, map wf, filter-concat, IdLnk wf, Knd wf, ma-state wf, fpf wf, fpf-trivial-subtype-top, idlnk-deq wf, Kind-deq wf, product-deq wf, fpf-dom wf, msga wf